Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	and(true,X)	→ activate(X)
2:	and(false,Y)	→ false
3:	if(true,X,Y)	→ activate(X)
4:	if(false,X,Y)	→ activate(Y)
5:	add(0,X)	→ activate(X)
6:	add(s(X),Y)	→ s(n__add(activate(X),activate(Y)))
7:	first(0,X)	→ nil
8:	first(s(X),cons(Y,Z))	→ cons(activate(Y),n__first(activate(X),activate(Z)))
9:	from(X)	→ cons(activate(X),n__from(n__s(activate(X))))
10:	add(X1,X2)	→ n__add(X1,X2)
11:	first(X1,X2)	→ n__first(X1,X2)
12:	from(X)	→ n__from(X)
13:	s(X)	→ n__s(X)
14:	activate(n__add(X1,X2))	→ add(X1,X2)
15:	activate(n__first(X1,X2))	→ first(X1,X2)
16:	activate(n__from(X))	→ from(X)
17:	activate(n__s(X))	→ s(X)
18:	activate(X)	→ X

There are 15 dependency pairs:

The approximated dependency graph contains one SCC: {22,24-32}.

Consider the SCC {22,24-32}. There are no usable rules. By taking the AF π with π(ACTIVATE) = π(FROM) = π(n__from) = π(s) = 1 together with the lexicographic path order with precedence n__add ≻ ADD and n__first ≻ FIRST, the rules in {29,32} are weakly decreasing and the rules in {22,24-28,30,31} are strictly decreasing. There is one new SCC.
- Consider the SCC {29,32}. By taking the AF π with π(ACTIVATE) = π(FROM) = 1 together with the lexicographic path order with empty precedence, rule 29 is weakly decreasing and rule 32 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.05 seconds) --- May 3, 2006